T:Type, eq:EqDecider(T), as, bs:T List.
(x:T. (x  list-diff(eq;as;bs))  (x  as) & (x  bs))
& (no_repeats(T;as)  no_repeats(T;list-diff(eq;as;bs))) 

latex

Definitions	(x  l), A, P & Q, P  Q, x:A. B(x), no_repeats(T;l), P  Q, t  T, EqDecider(T), Prop, P  Q, deq-member(eq;x;L), b, b, x. t(x), filter(P;l), list-diff(eq;as;bs)
Lemmas	no repeats wf, no repeats filter, member filter, filter wf, all functionality wrt iff, iff functionality wrt iff, and functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, iff wf, bnot wf, assert wf, deq-member wf, not wf, l member wf, deq wf